<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>SeqAssigner</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="SeqAssigner";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/Section.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/SeqAssigner.html" target="_top">Frames</a></li>
<li><a href="SeqAssigner.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class SeqAssigner" class="title">Class SeqAssigner</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.lang.SeqAssigner</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>All Implemented Interfaces:</dt>
<dd><a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">SeqAssigner</span>
extends java.lang.Object
implements <a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a></pre>
<div class="block">The <code>SeqAssigner</code> generates sequence numbers for Metamath objects
 (MObj) within the mmj2 Logical System.
 <p>
 SeqAssigner.java's job is assigning sequence numbers to Metamath objects
 (MObj's) as they are loaded and inserted in the mmj2 Logical System. Sequence
 numbers are assigned sequentially and provide the basis for the mechanism
 which ensures that cyclic or forward references by Metamath objects are
 rejected (as invalid).
 <p>
 The motivation for this new feature is assignment of sequence numbers for
 theorems inserted by the new Theorem Loader enhancement. Previously all
 Metamath objects were appended to the "end" of the Logical System and
 sequence numbers were assigned from 10 by 10 up to the maximum of 2**31 - 1.
 <p>
 The Theorem Loader aims to "insert" theorems and logical hypotheses into the
 sequence number "gaps" left over from the initial Metamath .mm file load(s)
 (RunParm "LoadFile").
 <p>
 The Theorem Loader determines the Metamath object dependencies of objects to
 be inserted and instructs SeqAssigner to assign in the gap after the
 referenced object with the highest sequence number. The SeqAssigner
 determines whether or not the "gap" is full and assigns the appropriate
 sequence number for each new object. A full gap results in an "append"ed
 sequence number, which may or may not be suitable -- if a new theorem is
 referred to by an existing theorem, then appending the new theorem is not
 acceptable (which results in an error and backout of all changes prior to
 detection of the error.)
 <p>
 Associated with SeqAssigner.java is a new RunParm,
 
 <pre>
      SeqAssignerIntervalSize,9999
 </pre>
 
 The default sequence number interval is 1000, thus allowing for 999 inserts
 into every gap. It also provides the capability to load at least 1 million
 Metamath objects (perhaps more) into the mmj2 Logical System. An interval
 size of 100 would be suitable for almost every purpose -- the exception being
 automated updates from an external system via the new "mmj2 Service" feature.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/SeqAssigner.html#SeqAssigner()">SeqAssigner</a></strong>()</code>
<div class="block">Construct with default set of parameters.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/SeqAssigner.html#SeqAssigner(int, int)">SeqAssigner</a></strong>(int&nbsp;intervalSize,
           int&nbsp;intervalTblInitialSize)</code>
<div class="block">Construct with full set of parameters.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/SeqAssigner.html#commit(mmj.tl.MMTTheoremSet)">commit</a></strong>(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet)</code>
<div class="block">Bit of a misnomer as this function merely turns off checkpointing.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/SeqAssigner.html#nextInsertSeq(int)">nextInsertSeq</a></strong>(int&nbsp;locAfterSeq)</code>
<div class="block">Constructs MObj.seq value for a Metamath object to be inserted in the
 number gap between two existing object.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/SeqAssigner.html#nextSeq()">nextSeq</a></strong>()</code>
<div class="block">Constructs MObj.seq value for new object.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/SeqAssigner.html#rollback(mmj.tl.MMTTheoremSet, mmj.lang.Messages, boolean)">rollback</a></strong>(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet,
        <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
        boolean&nbsp;auditMessages)</code>
<div class="block">Reverses all changes made to the SeqAssigner state variables since the
 last checkpoing was taken.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/SeqAssigner.html#turnOnCheckpointing()">turnOnCheckpointing</a></strong>()</code>
<div class="block">Bit of a misnomer as this function takes a checkpoint in case a rollback
 is needed by TheoremLoader.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/SeqAssigner.html#validateIntervalSize(int)">validateIntervalSize</a></strong>(int&nbsp;n)</code>
<div class="block">Validates Interval Size parameter.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/SeqAssigner.html#validateIntervalTblInitialSize(int)">validateIntervalTblInitialSize</a></strong>(int&nbsp;n)</code>
<div class="block">Validates Interval Table Initial Size parameter.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="SeqAssigner()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>SeqAssigner</h4>
<pre>public&nbsp;SeqAssigner()</pre>
<div class="block">Construct with default set of parameters.</div>
</li>
</ul>
<a name="SeqAssigner(int, int)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>SeqAssigner</h4>
<pre>public&nbsp;SeqAssigner(int&nbsp;intervalSize,
           int&nbsp;intervalTblInitialSize)</pre>
<div class="block">Construct with full set of parameters.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>intervalSize</code> - numbering interval for MObj.seq numbers.</dd><dd><code>intervalTblInitialSize</code> - initial size of HashMap for recording
            insertions in the sequence number interval gaps.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="validateIntervalSize(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>validateIntervalSize</h4>
<pre>public static&nbsp;void&nbsp;validateIntervalSize(int&nbsp;n)</pre>
<div class="block">Validates Interval Size parameter.
 <p>
 Provided this function so that the same code can be used by
 LogicalSystemBoss.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>n</code> - interval size for MObj.seq numbers.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if invalid interval size.</dd></dl>
</li>
</ul>
<a name="validateIntervalTblInitialSize(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>validateIntervalTblInitialSize</h4>
<pre>public static&nbsp;void&nbsp;validateIntervalTblInitialSize(int&nbsp;n)</pre>
<div class="block">Validates Interval Table Initial Size parameter.
 <p>
 Provided this function so that the same code can be used by
 LogicalSystemBoss.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>n</code> - interval table initial size for MObj.seq numbers.</dd></dl>
</li>
</ul>
<a name="nextSeq()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>nextSeq</h4>
<pre>public&nbsp;int&nbsp;nextSeq()</pre>
<div class="block">Constructs MObj.seq value for new object.
 <p>
 The return number is one of the "appended" sequence numbers, located
 logically at the end of LogicalSystem.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>new MObj.seq number.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if the next available sequence number is
             beyond the number range available to a Java "int".</dd></dl>
</li>
</ul>
<a name="nextInsertSeq(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>nextInsertSeq</h4>
<pre>public&nbsp;int&nbsp;nextInsertSeq(int&nbsp;locAfterSeq)</pre>
<div class="block">Constructs MObj.seq value for a Metamath object to be inserted in the
 number gap between two existing object.
 <p>
 The return number is one of the "inserted" sequence numbers, located
 logically at the end of LogicalSystem.
 <p>
 The input locAfterSeq designates a an "interval" which contains the "gap"
 of numbers (e.g. seq 3501 is in the 35 interval which has gap 3501 thru
 3599.) The inserted sequence number goes into this gap if the gap is not
 already full. (A HashMap of BitSet is used to keep track of the intervals
 and gaps, respectively.)
 <p>
 To conserve empty gap space, if the locAfterSeq is assigned to the last
 interval in the system, then the next sequence number is not inserted,
 but appended.
 <p>
 If the next sequence number is not inserted (meaning that it is to be
 appended), then -1 is returned instead of the assigned sequence number.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>locAfterSeq</code> - see description</dd>
<dt><span class="strong">Returns:</span></dt><dd>new MObj.seq number if number was inserted, else -1 indicating
         that it must be appended.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if the next available sequence number is
             beyond the number range available to a Java "int".</dd></dl>
</li>
</ul>
<a name="turnOnCheckpointing()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>turnOnCheckpointing</h4>
<pre>public&nbsp;void&nbsp;turnOnCheckpointing()</pre>
<div class="block">Bit of a misnomer as this function takes a checkpoint in case a rollback
 is needed by TheoremLoader.</div>
<dl><dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if checkpointing is already on.</dd></dl>
</li>
</ul>
<a name="commit(mmj.tl.MMTTheoremSet)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>commit</h4>
<pre>public&nbsp;void&nbsp;commit(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet)</pre>
<div class="block">Bit of a misnomer as this function merely turns off checkpointing.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/tl/TheoremLoaderCommitListener.html#commit(mmj.tl.MMTTheoremSet)">commit</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>mmtTheoremSet</code> - Set of TheoremStmtGroup updates now committed</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if checkpointing is not already on.</dd></dl>
</li>
</ul>
<a name="rollback(mmj.tl.MMTTheoremSet, mmj.lang.Messages, boolean)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>rollback</h4>
<pre>public&nbsp;void&nbsp;rollback(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet,
            <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
            boolean&nbsp;auditMessages)</pre>
<div class="block">Reverses all changes made to the SeqAssigner state variables since the
 last checkpoing was taken.
 <p>
 Notice that only inserted sequence numbers are individually backed out.
 Appended sequence numbers are backed out en masse by reverting to the
 checkpointed value of "nbrIntervals" -- that is because there is no
 BitSet created for an interval until there is an insert in the interval's
 gap.
 <p>
 Audit messages are produced primarily so that the code is testable --
 they provide "instrumentation".</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mmtTheoremSet</code> - TheoremLoader's set of adds and updates.</dd><dd><code>messages</code> - the Messages object for error logging</dd><dd><code>auditMessages</code> - true to write audit messages</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if a checkpoint was not taken prior to
             the rollback request.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/Section.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/SeqAssigner.html" target="_top">Frames</a></li>
<li><a href="SeqAssigner.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
